A:Type, B:(AType), eq:EqDecider(A), f, g:a:A fp B(a). f || g  f  g  g  f 

latex

Definitions	f || g, EqDecider(T), f  g, P  Q, A c B, f(x), b, x  dom(f), f  g, a:A fp B(a), Top, x. t(x), x:A. B(x), x(s), t  T, P  Q, P & Q, P  Q, {T}, P  Q, if b then t else f fi , Unit, , , b, A, False
Lemmas	not wf, bnot wf, bool wf, fpf-ap wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, fpf-join-ap-sq, fpf-join-dom, fpf-trivial-subtype-top, top wf, fpf-join wf, fpf-dom wf, assert wf, deq wf, fpf wf, fpf-compatible wf